package srt.tool;

import java.util.ArrayList;
import java.util.List;

import srt.ast.AssertStmt;
import srt.ast.AssumeStmt;
import srt.ast.BinaryExpr;
import srt.ast.BlockStmt;
import srt.ast.DeclRef;
import srt.ast.EmptyStmt;
import srt.ast.Expr;
import srt.ast.IfStmt;
import srt.ast.IntLiteral;
import srt.ast.Invariant;
import srt.ast.Stmt;
import srt.ast.UnaryExpr;
import srt.ast.WhileStmt;
import srt.ast.visitor.impl.DefaultVisitor;

//Implementation of bmc mode
public class LoopUnwinderVisitor extends DefaultVisitor {

	private boolean unsound;
	private int defaultUnwindBound;

	public LoopUnwinderVisitor(boolean unsound, int defaultUnwindBound) {
		super(true);
		this.unsound = unsound;
		this.defaultUnwindBound = defaultUnwindBound;
	}

	@Override
	public Object visit(WhileStmt whileStmt) {

		int bound = defaultUnwindBound;
		if (whileStmt.getBound() != null) {
			bound = whileStmt.getBound().getValue();
		}

		List<Stmt> statementsStack = new ArrayList<Stmt>();
		
		Expr whileCond = null;
		
		try{
			whileCond = (BinaryExpr) whileStmt.getCondition();
		} catch (ClassCastException e){
			whileCond = (DeclRef) whileStmt.getCondition();
		}

		for(Invariant i : whileStmt.getInvariantList().getInvariants()){
			statementsStack.add(new AssertStmt(i.getExpr()));
		}
		
		//bound = 0 case, create last if statement with assume(!c) and assert(!c) if unsound
		if (bound == 0) {
			
			List<Stmt> endingIf = new ArrayList<Stmt>();
			
			if (!unsound) {
				endingIf.add(new AssertStmt(new UnaryExpr(
						UnaryExpr.LNOT, whileCond), whileStmt.getNodeInfo()));
			}

			endingIf.add(new AssumeStmt(new UnaryExpr(UnaryExpr.LNOT,
					whileCond), whileStmt.getNodeInfo()));
			
			statementsStack.add(new IfStmt(whileCond, new BlockStmt(endingIf), new EmptyStmt()));
			
			return new BlockStmt(statementsStack, whileStmt.getNodeInfo());
		}
		
		//create if statement, add loop body and assertions, run visit again on the loop
		Stmt ifBody;

		ifBody = (Stmt) visit(new WhileStmt(whileCond, new IntLiteral(bound-1),
				whileStmt.getInvariantList(), whileStmt.getBody(),
				whileStmt.getNodeInfo()));
		
		List<Stmt> temporarryBlock = new ArrayList<Stmt>();
		
		temporarryBlock.add((Stmt) visit(whileStmt.getBody()));
		
		
		
		temporarryBlock.add(ifBody);
		

		statementsStack.add(new IfStmt(whileCond, new BlockStmt(temporarryBlock),
				new EmptyStmt()));

		return new BlockStmt(statementsStack, whileStmt.getNodeInfo());
	}

}
